Static program analysis often must deal with opaque code, or parts of a program that are either not available (e.g., due to missing source code), or too complex for analysis. For example, a static analysis of JavaScript code may need to analyze built-in and library code, since JavaScript's standard library is built into the runtime systems that implement the JavaScript language. Manually-generated models are commonly used to model opaque code, but manual approaches are time-consuming and error-prone. Automatic modeling techniques are often too imprecise to be useful when modeling opaque code represented in a high-level, dynamic language, such as JavaScript. For example, automatic modeling techniques based on specifications represented in natural language depend heavily on the quality and format of the available specifications. And automatic modeling techniques based on dynamic traces resulting from the execution of opaque code are limited to semantics that are observable in the traces.